#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <sys/time.h>
#include <unistd.h>
#include <pthread.h>
#include <Judy.h>

#include "model/globals.h"
#include "model/initialization.h"
#include "model/print_utils.h"
#include "normalization/normalization.h"
#include "normalization/globals.h"
#include "normalization/print_utils.h"
#include "preprocessing/preprocessing.h"
#include "completion/completion.h"
#include "completion/print_utils.h"
#include "hierarchy/globals.h"
#include "hierarchy/print_utils.h"

extern int yyparse(void);
extern FILE *yyin;

struct timeval tStart, tEnd;
#define START_TIMER	gettimeofday(&tStart, NULL)
#define STOP_TIMER	gettimeofday(&tEnd, NULL)
#define TIME_DIFF	(((double)tEnd.tv_sec * 1000000.0 + \
	(double)tEnd.tv_usec) - \
	((double)tStart.tv_sec * 1000000.0 + (double)tStart.tv_usec) )


int main(int argc, char *argv[]) {
	int parser;
	FILE* hierarchy_out;
	double total_time = 0.0;

	if (argc <= 2) {
		fprintf(stderr,"syntax: %s input_kb output_hierarchy\n", argv[0]);
		return -1;
	}

	yyin = fopen(argv[1], "r");
	assert(yyin != NULL);

	// printf("Initializing ELC...");
	init();
	// printf("\tdone\n");

	printf("Loading KB...");
	fflush(stdout);
	START_TIMER;
	parser = yyparse();
	STOP_TIMER;
	if (parser != 0) {	
		print_short_stats();
		fprintf(stderr,"aborting\n");
		exit(-1);
	}
	total_time += TIME_DIFF;
	printf("\tdone in %.3f milisecs\n", TIME_DIFF / 1000);
	print_short_stats();
	// printf("-------EquivalentClass Axioms---------\n");
	// print_eqclass_axioms();
	// printf("-------SubClass Axioms---------\n");
	// print_subclass_axioms();
	// printf("------- Axioms---------\n");
	// print_axioms(tbox.axioms,tbox.axiom_count);

	// printf("Normalizing KB on %d core(s)...",core_count);
	printf("Normalizing KB ...");
	fflush(stdout);
	START_TIMER;
	normalize_tbox(tbox,&normalized_tbox);
	STOP_TIMER;
	total_time += TIME_DIFF;
	printf("\tdone in %.3f milisecs\n", TIME_DIFF / 1000);
	print_normalization_stats();
	// printf("------- Normalized Axioms---------\n");
	// print_normalized_tbox();
	// realloc space for original axioms and normalized axioms
	// for shrinking the dynamic arrays to the actual number of original
	// and normalized axioms
	// reInit();
	// after normalization original axioms are not needed any more, free them
	free_original_kb();

	printf("Preprocessing the normalized KB ...");
	START_TIMER;
	preprocess();
	STOP_TIMER;
	total_time += TIME_DIFF;
	printf("\tdone in %.3f milisecs\n", TIME_DIFF / 1000);

	printf("Completing the normalized KB ...");
	fflush(stdout);
	START_TIMER;
	complete_kb();
	STOP_TIMER;
	total_time += TIME_DIFF;
	printf("\tdone in %.3f milisecs\n", TIME_DIFF / 1000);

	// print_subsumer_lists();

	printf("Computing the concept hierarchy ...");
	fflush(stdout);
	START_TIMER;
	compute_concept_hierarchy();
	STOP_TIMER;
	total_time += TIME_DIFF;
	printf("\tdone in %.3f milisecs\n", TIME_DIFF / 1000);


	hierarchy_out = fopen(argv[2], "w");
	assert(hierarchy_out != NULL);

	print_concept_hierarchy(hierarchy_out);
	fclose(hierarchy_out);

	printf("Total time: %.3f milisecs\n", total_time / 1000);
	getchar();

	return 0;
}

